the_w:World, l:IdLnk, mss:(Msg List). withlnk(l;mss)  ((t:Id  (the_w.M(l,t))) List) 

latex

Definitions	x:A. B(x), Msg, t  T, w.M, withlnk(l;mss), t.1, t.2, World, , Msg(M), mlnk(m), P  Q, P  Q, P & Q
Lemmas	mapfilter wf, Msg wf, eq lnk wf, mlnk wf, Id wf, assert wf, IdLnk wf, world wf, assert-eq-lnk